0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 184 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 348 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 4 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 MRRProof (⇔, 199 ms)
↳27 QDP
↳28 DependencyGraphProof (⇔, 0 ms)
↳29 QDP
↳30 UsableRulesProof (⇔, 0 ms)
↳31 QDP
↳32 QReductionProof (⇔, 0 ms)
↳33 QDP
↳34 QDPSizeChangeProof (⇔, 0 ms)
↳35 YES
↳36 PiDP
↳37 UsableRulesProof (⇔, 0 ms)
↳38 PiDP
↳39 PiDPToQDPProof (⇒, 0 ms)
↳40 QDP
↳41 QDPSizeChangeProof (⇔, 0 ms)
↳42 YES
↳43 PiDP
↳44 UsableRulesProof (⇔, 0 ms)
↳45 PiDP
↳46 PiDPToQDPProof (⇒, 0 ms)
↳47 QDP
↳48 Rewriting (⇔, 60 ms)
↳49 QDP
↳50 Rewriting (⇔, 0 ms)
↳51 QDP
↳52 QDPQMonotonicMRRProof (⇔, 732 ms)
↳53 QDP
↳54 DependencyGraphProof (⇔, 0 ms)
↳55 TRUE
↳56 PiDP
↳57 UsableRulesProof (⇔, 0 ms)
↳58 PiDP
↳59 PiDPToQDPProof (⇒, 0 ms)
↳60 QDP
↳61 Rewriting (⇔, 0 ms)
↳62 QDP
↳63 UsableRulesProof (⇔, 0 ms)
↳64 QDP
↳65 QReductionProof (⇔, 0 ms)
↳66 QDP
↳67 QDPQMonotonicMRRProof (⇔, 27 ms)
↳68 QDP
↳69 DependencyGraphProof (⇔, 0 ms)
↳70 TRUE
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U18_GA(X1, X2, X3, X4, splitD_in_ggaa(X2, X3, X5, X6))
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → SPLITD_IN_GGAA(X2, X3, X5, X6)
SPLITD_IN_GGAA(X1, X2, .(X1, X3), X4) → U2_GGAA(X1, X2, X3, X4, splitA_in_gaa(X2, X4, X3))
SPLITD_IN_GGAA(X1, X2, .(X1, X3), X4) → SPLITA_IN_GAA(X2, X4, X3)
SPLITA_IN_GAA(.(X1, X2), .(X1, X3), X4) → U1_GAA(X1, X2, X3, X4, splitA_in_gaa(X2, X4, X3))
SPLITA_IN_GAA(.(X1, X2), .(X1, X3), X4) → SPLITA_IN_GAA(X2, X4, X3)
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U19_GA(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U19_GA(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U20_GA(X1, X2, X3, X4, mergesortB_in_ga(.(X1, X6), X7))
U19_GA(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6), X7)
U19_GA(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U21_GA(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U21_GA(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U22_GA(X1, X2, X3, X4, mergesortE_in_ga(X5, X8))
U21_GA(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → MERGESORTE_IN_GA(X5, X8)
MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → U3_GA(X1, X2, X3, X4, splitD_in_ggaa(X1, .(X2, X3), X5, X6))
MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → SPLITD_IN_GGAA(X1, .(X2, X3), X5, X6)
MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → U4_GA(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U4_GA(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U5_GA(X1, X2, X3, X4, mergesortE_in_ga(X5, X7))
U4_GA(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → MERGESORTE_IN_GA(X5, X7)
U4_GA(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U6_GA(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U7_GA(X1, X2, X3, X4, mergesortE_in_ga(X6, X8))
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6, X8)
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U8_GA(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U8_GA(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U9_GA(X1, X2, X3, X4, mergeC_in_gga(X7, X8, X4))
U8_GA(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → MERGEC_IN_GGA(X7, X8, X4)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U10_GGA(X1, X2, X3, X4, X5, leF_in_gg(X1, X3))
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → LEF_IN_GG(X1, X3)
LEF_IN_GG(s(X1), s(X2)) → U16_GG(X1, X2, leF_in_gg(X1, X2))
LEF_IN_GG(s(X1), s(X2)) → LEF_IN_GG(X1, X2)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U11_GGA(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
U11_GGA(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U12_GGA(X1, X2, X3, X4, X5, mergeC_in_gga(X2, .(X3, X4), X5))
U11_GGA(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → MERGEC_IN_GGA(X2, .(X3, X4), X5)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U13_GGA(X1, X2, X3, X4, X5, gtG_in_gg(X1, X3))
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → GTG_IN_GG(X1, X3)
GTG_IN_GG(s(X1), s(X2)) → U17_GG(X1, X2, gtG_in_gg(X1, X2))
GTG_IN_GG(s(X1), s(X2)) → GTG_IN_GG(X1, X2)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U14_GGA(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
U14_GGA(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U15_GGA(X1, X2, X3, X4, X5, mergeC_in_gga(.(X1, X2), X4, X5))
U14_GGA(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4, X5)
U21_GA(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U23_GA(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
U23_GA(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U24_GA(X1, X2, X3, X4, mergeC_in_gga(X7, X8, X4))
U23_GA(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → MERGEC_IN_GGA(X7, X8, X4)
splitcD_in_ggaa(X1, X2, .(X1, X3), X4) → U31_ggaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U26_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U26_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U31_ggaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U28_ga(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U28_ga(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U29_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U32_ga(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U32_ga(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U33_ga(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U34_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U36_gga(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U36_gga(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U38_gga(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
U38_gga(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U39_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U37_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U35_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U29_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U30_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U30_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U18_GA(X1, X2, X3, X4, splitD_in_ggaa(X2, X3, X5, X6))
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → SPLITD_IN_GGAA(X2, X3, X5, X6)
SPLITD_IN_GGAA(X1, X2, .(X1, X3), X4) → U2_GGAA(X1, X2, X3, X4, splitA_in_gaa(X2, X4, X3))
SPLITD_IN_GGAA(X1, X2, .(X1, X3), X4) → SPLITA_IN_GAA(X2, X4, X3)
SPLITA_IN_GAA(.(X1, X2), .(X1, X3), X4) → U1_GAA(X1, X2, X3, X4, splitA_in_gaa(X2, X4, X3))
SPLITA_IN_GAA(.(X1, X2), .(X1, X3), X4) → SPLITA_IN_GAA(X2, X4, X3)
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U19_GA(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U19_GA(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U20_GA(X1, X2, X3, X4, mergesortB_in_ga(.(X1, X6), X7))
U19_GA(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6), X7)
U19_GA(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U21_GA(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U21_GA(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U22_GA(X1, X2, X3, X4, mergesortE_in_ga(X5, X8))
U21_GA(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → MERGESORTE_IN_GA(X5, X8)
MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → U3_GA(X1, X2, X3, X4, splitD_in_ggaa(X1, .(X2, X3), X5, X6))
MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → SPLITD_IN_GGAA(X1, .(X2, X3), X5, X6)
MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → U4_GA(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U4_GA(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U5_GA(X1, X2, X3, X4, mergesortE_in_ga(X5, X7))
U4_GA(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → MERGESORTE_IN_GA(X5, X7)
U4_GA(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U6_GA(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U7_GA(X1, X2, X3, X4, mergesortE_in_ga(X6, X8))
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6, X8)
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U8_GA(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U8_GA(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U9_GA(X1, X2, X3, X4, mergeC_in_gga(X7, X8, X4))
U8_GA(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → MERGEC_IN_GGA(X7, X8, X4)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U10_GGA(X1, X2, X3, X4, X5, leF_in_gg(X1, X3))
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → LEF_IN_GG(X1, X3)
LEF_IN_GG(s(X1), s(X2)) → U16_GG(X1, X2, leF_in_gg(X1, X2))
LEF_IN_GG(s(X1), s(X2)) → LEF_IN_GG(X1, X2)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U11_GGA(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
U11_GGA(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U12_GGA(X1, X2, X3, X4, X5, mergeC_in_gga(X2, .(X3, X4), X5))
U11_GGA(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → MERGEC_IN_GGA(X2, .(X3, X4), X5)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U13_GGA(X1, X2, X3, X4, X5, gtG_in_gg(X1, X3))
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → GTG_IN_GG(X1, X3)
GTG_IN_GG(s(X1), s(X2)) → U17_GG(X1, X2, gtG_in_gg(X1, X2))
GTG_IN_GG(s(X1), s(X2)) → GTG_IN_GG(X1, X2)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U14_GGA(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
U14_GGA(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U15_GGA(X1, X2, X3, X4, X5, mergeC_in_gga(.(X1, X2), X4, X5))
U14_GGA(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4, X5)
U21_GA(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U23_GA(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
U23_GA(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U24_GA(X1, X2, X3, X4, mergeC_in_gga(X7, X8, X4))
U23_GA(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → MERGEC_IN_GGA(X7, X8, X4)
splitcD_in_ggaa(X1, X2, .(X1, X3), X4) → U31_ggaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U26_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U26_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U31_ggaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U28_ga(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U28_ga(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U29_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U32_ga(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U32_ga(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U33_ga(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U34_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U36_gga(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U36_gga(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U38_gga(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
U38_gga(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U39_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U37_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U35_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U29_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U30_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U30_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)
GTG_IN_GG(s(X1), s(X2)) → GTG_IN_GG(X1, X2)
splitcD_in_ggaa(X1, X2, .(X1, X3), X4) → U31_ggaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U26_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U26_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U31_ggaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U28_ga(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U28_ga(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U29_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U32_ga(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U32_ga(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U33_ga(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U34_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U36_gga(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U36_gga(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U38_gga(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
U38_gga(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U39_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U37_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U35_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U29_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U30_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U30_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)
GTG_IN_GG(s(X1), s(X2)) → GTG_IN_GG(X1, X2)
GTG_IN_GG(s(X1), s(X2)) → GTG_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
LEF_IN_GG(s(X1), s(X2)) → LEF_IN_GG(X1, X2)
splitcD_in_ggaa(X1, X2, .(X1, X3), X4) → U31_ggaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U26_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U26_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U31_ggaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U28_ga(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U28_ga(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U29_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U32_ga(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U32_ga(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U33_ga(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U34_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U36_gga(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U36_gga(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U38_gga(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
U38_gga(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U39_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U37_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U35_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U29_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U30_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U30_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)
LEF_IN_GG(s(X1), s(X2)) → LEF_IN_GG(X1, X2)
LEF_IN_GG(s(X1), s(X2)) → LEF_IN_GG(X1, X2)
From the DPs we obtained the following set of size-change graphs:
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U11_GGA(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
U11_GGA(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → MERGEC_IN_GGA(X2, .(X3, X4), X5)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U14_GGA(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
U14_GGA(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4, X5)
splitcD_in_ggaa(X1, X2, .(X1, X3), X4) → U31_ggaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U26_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U26_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U31_ggaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U28_ga(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U28_ga(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U29_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U32_ga(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U32_ga(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U33_ga(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U34_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U36_gga(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U36_gga(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U38_gga(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
U38_gga(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U39_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U37_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U35_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U29_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U30_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U30_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X1, X5)) → U11_GGA(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
U11_GGA(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → MERGEC_IN_GGA(X2, .(X3, X4), X5)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4), .(X3, X5)) → U14_GGA(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
U14_GGA(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4, X5)
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U11_GGA(X1, X2, X3, X4, lecF_in_gg(X1, X3))
U11_GGA(X1, X2, X3, X4, lecF_out_gg(X1, X3)) → MERGEC_IN_GGA(X2, .(X3, X4))
MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U14_GGA(X1, X2, X3, X4, gtcG_in_gg(X1, X3))
U14_GGA(X1, X2, X3, X4, gtcG_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4)
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
lecF_in_gg(x0, x1)
gtcG_in_gg(x0, x1)
U40_gg(x0, x1, x2)
U41_gg(x0, x1, x2)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U11_GGA(X1, X2, X3, X4, lecF_in_gg(X1, X3))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
POL(.(x1, x2)) = 1 + 2·x1 + x2
POL(0) = 0
POL(MERGEC_IN_GGA(x1, x2)) = 2·x1 + 2·x2
POL(U11_GGA(x1, x2, x3, x4, x5)) = 2 + x1 + 2·x2 + 2·x3 + 2·x4 + x5
POL(U14_GGA(x1, x2, x3, x4, x5)) = 2 + 2·x1 + 2·x2 + 2·x3 + 2·x4 + 2·x5
POL(U40_gg(x1, x2, x3)) = 2·x1 + 2·x2 + x3
POL(U41_gg(x1, x2, x3)) = x1 + x2 + x3
POL(gtcG_in_gg(x1, x2)) = 1 + x1 + x2
POL(gtcG_out_gg(x1, x2)) = x1 + x2
POL(lecF_in_gg(x1, x2)) = 2·x1 + 2·x2
POL(lecF_out_gg(x1, x2)) = 2·x1 + 2·x2
POL(s(x1)) = 2·x1
U11_GGA(X1, X2, X3, X4, lecF_out_gg(X1, X3)) → MERGEC_IN_GGA(X2, .(X3, X4))
MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U14_GGA(X1, X2, X3, X4, gtcG_in_gg(X1, X3))
U14_GGA(X1, X2, X3, X4, gtcG_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4)
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
lecF_in_gg(x0, x1)
gtcG_in_gg(x0, x1)
U40_gg(x0, x1, x2)
U41_gg(x0, x1, x2)
U14_GGA(X1, X2, X3, X4, gtcG_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U14_GGA(X1, X2, X3, X4, gtcG_in_gg(X1, X3))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
lecF_in_gg(x0, x1)
gtcG_in_gg(x0, x1)
U40_gg(x0, x1, x2)
U41_gg(x0, x1, x2)
U14_GGA(X1, X2, X3, X4, gtcG_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U14_GGA(X1, X2, X3, X4, gtcG_in_gg(X1, X3))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
lecF_in_gg(x0, x1)
gtcG_in_gg(x0, x1)
U40_gg(x0, x1, x2)
U41_gg(x0, x1, x2)
lecF_in_gg(x0, x1)
U40_gg(x0, x1, x2)
U14_GGA(X1, X2, X3, X4, gtcG_out_gg(X1, X3)) → MERGEC_IN_GGA(.(X1, X2), X4)
MERGEC_IN_GGA(.(X1, X2), .(X3, X4)) → U14_GGA(X1, X2, X3, X4, gtcG_in_gg(X1, X3))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
gtcG_in_gg(x0, x1)
U41_gg(x0, x1, x2)
From the DPs we obtained the following set of size-change graphs:
SPLITA_IN_GAA(.(X1, X2), .(X1, X3), X4) → SPLITA_IN_GAA(X2, X4, X3)
splitcD_in_ggaa(X1, X2, .(X1, X3), X4) → U31_ggaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U26_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U26_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U31_ggaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U28_ga(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U28_ga(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U29_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U32_ga(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U32_ga(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U33_ga(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U34_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U36_gga(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U36_gga(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U38_gga(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
U38_gga(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U39_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U37_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U35_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U29_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U30_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U30_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)
SPLITA_IN_GAA(.(X1, X2), .(X1, X3), X4) → SPLITA_IN_GAA(X2, X4, X3)
SPLITA_IN_GAA(.(X1, X2)) → SPLITA_IN_GAA(X2)
From the DPs we obtained the following set of size-change graphs:
MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → U4_GA(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U4_GA(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → MERGESORTE_IN_GA(X5, X7)
U4_GA(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U6_GA(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6, X8)
splitcD_in_ggaa(X1, X2, .(X1, X3), X4) → U31_ggaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U26_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U26_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U31_ggaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U28_ga(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U28_ga(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U29_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U32_ga(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U32_ga(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U33_ga(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U34_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U36_gga(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U36_gga(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U38_gga(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
U38_gga(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U39_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U37_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U35_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U29_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U30_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U30_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)
MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → U4_GA(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U4_GA(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → MERGESORTE_IN_GA(X5, X7)
U4_GA(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U6_GA(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6, X8)
splitcD_in_ggaa(X1, X2, .(X1, X3), X4) → U31_ggaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U32_ga(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U31_ggaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
U32_ga(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U26_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U33_ga(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U26_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U34_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U35_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U36_gga(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U38_gga(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
U36_gga(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
U38_gga(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U37_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U39_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
MERGESORTE_IN_GA(.(X1, .(X2, X3))) → U4_GA(X1, X2, X3, splitcD_in_ggaa(X1, .(X2, X3)))
U4_GA(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → MERGESORTE_IN_GA(X5)
U4_GA(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U6_GA(X1, X2, X3, X6, mergesortcE_in_ga(X5))
U6_GA(X1, X2, X3, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6)
splitcD_in_ggaa(X1, X2) → U31_ggaa(X1, X2, splitcA_in_gaa(X2))
mergesortcE_in_ga([]) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3))) → U32_ga(X1, X2, X3, splitcD_in_ggaa(X1, .(X2, X3)))
U31_ggaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
U32_ga(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X6, mergesortcE_in_ga(X5))
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, splitcA_in_gaa(X2))
U33_ga(X1, X2, X3, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X7, mergesortcE_in_ga(X6))
U26_gaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U34_ga(X1, X2, X3, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, mergecC_in_gga(X7, X8))
U35_ga(X1, X2, X3, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
mergecC_in_gga(X1, []) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga([], X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(.(X1, X2), .(X3, X4)) → U36_gga(X1, X2, X3, X4, lecF_in_gg(X1, X3))
mergecC_in_gga(.(X1, X2), .(X3, X4)) → U38_gga(X1, X2, X3, X4, gtcG_in_gg(X1, X3))
U36_gga(X1, X2, X3, X4, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, mergecC_in_gga(X2, .(X3, X4)))
U38_gga(X1, X2, X3, X4, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, mergecC_in_gga(.(X1, X2), X4))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U37_gga(X1, X2, X3, X4, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U39_gga(X1, X2, X3, X4, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
splitcD_in_ggaa(x0, x1)
mergesortcE_in_ga(x0)
U31_ggaa(x0, x1, x2)
U32_ga(x0, x1, x2, x3)
splitcA_in_gaa(x0)
U33_ga(x0, x1, x2, x3, x4)
U26_gaa(x0, x1, x2)
U34_ga(x0, x1, x2, x3, x4)
U35_ga(x0, x1, x2, x3)
mergecC_in_gga(x0, x1)
U36_gga(x0, x1, x2, x3, x4)
U38_gga(x0, x1, x2, x3, x4)
lecF_in_gg(x0, x1)
U37_gga(x0, x1, x2, x3, x4)
gtcG_in_gg(x0, x1)
U39_gga(x0, x1, x2, x3, x4)
U40_gg(x0, x1, x2)
U41_gg(x0, x1, x2)
MERGESORTE_IN_GA(.(X1, .(X2, X3))) → U4_GA(X1, X2, X3, U31_ggaa(X1, .(X2, X3), splitcA_in_gaa(.(X2, X3))))
U4_GA(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → MERGESORTE_IN_GA(X5)
U4_GA(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U6_GA(X1, X2, X3, X6, mergesortcE_in_ga(X5))
U6_GA(X1, X2, X3, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6)
MERGESORTE_IN_GA(.(X1, .(X2, X3))) → U4_GA(X1, X2, X3, U31_ggaa(X1, .(X2, X3), splitcA_in_gaa(.(X2, X3))))
splitcD_in_ggaa(X1, X2) → U31_ggaa(X1, X2, splitcA_in_gaa(X2))
mergesortcE_in_ga([]) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3))) → U32_ga(X1, X2, X3, splitcD_in_ggaa(X1, .(X2, X3)))
U31_ggaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
U32_ga(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X6, mergesortcE_in_ga(X5))
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, splitcA_in_gaa(X2))
U33_ga(X1, X2, X3, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X7, mergesortcE_in_ga(X6))
U26_gaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U34_ga(X1, X2, X3, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, mergecC_in_gga(X7, X8))
U35_ga(X1, X2, X3, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
mergecC_in_gga(X1, []) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga([], X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(.(X1, X2), .(X3, X4)) → U36_gga(X1, X2, X3, X4, lecF_in_gg(X1, X3))
mergecC_in_gga(.(X1, X2), .(X3, X4)) → U38_gga(X1, X2, X3, X4, gtcG_in_gg(X1, X3))
U36_gga(X1, X2, X3, X4, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, mergecC_in_gga(X2, .(X3, X4)))
U38_gga(X1, X2, X3, X4, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, mergecC_in_gga(.(X1, X2), X4))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U37_gga(X1, X2, X3, X4, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U39_gga(X1, X2, X3, X4, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
splitcD_in_ggaa(x0, x1)
mergesortcE_in_ga(x0)
U31_ggaa(x0, x1, x2)
U32_ga(x0, x1, x2, x3)
splitcA_in_gaa(x0)
U33_ga(x0, x1, x2, x3, x4)
U26_gaa(x0, x1, x2)
U34_ga(x0, x1, x2, x3, x4)
U35_ga(x0, x1, x2, x3)
mergecC_in_gga(x0, x1)
U36_gga(x0, x1, x2, x3, x4)
U38_gga(x0, x1, x2, x3, x4)
lecF_in_gg(x0, x1)
U37_gga(x0, x1, x2, x3, x4)
gtcG_in_gg(x0, x1)
U39_gga(x0, x1, x2, x3, x4)
U40_gg(x0, x1, x2)
U41_gg(x0, x1, x2)
MERGESORTE_IN_GA(.(X1, .(X2, X3))) → U4_GA(X1, X2, X3, U31_ggaa(X1, .(X2, X3), U26_gaa(X2, X3, splitcA_in_gaa(X3))))
U4_GA(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → MERGESORTE_IN_GA(X5)
U4_GA(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U6_GA(X1, X2, X3, X6, mergesortcE_in_ga(X5))
U6_GA(X1, X2, X3, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6)
MERGESORTE_IN_GA(.(X1, .(X2, X3))) → U4_GA(X1, X2, X3, U31_ggaa(X1, .(X2, X3), U26_gaa(X2, X3, splitcA_in_gaa(X3))))
splitcD_in_ggaa(X1, X2) → U31_ggaa(X1, X2, splitcA_in_gaa(X2))
mergesortcE_in_ga([]) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3))) → U32_ga(X1, X2, X3, splitcD_in_ggaa(X1, .(X2, X3)))
U31_ggaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
U32_ga(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X6, mergesortcE_in_ga(X5))
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, splitcA_in_gaa(X2))
U33_ga(X1, X2, X3, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X7, mergesortcE_in_ga(X6))
U26_gaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U34_ga(X1, X2, X3, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, mergecC_in_gga(X7, X8))
U35_ga(X1, X2, X3, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
mergecC_in_gga(X1, []) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga([], X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(.(X1, X2), .(X3, X4)) → U36_gga(X1, X2, X3, X4, lecF_in_gg(X1, X3))
mergecC_in_gga(.(X1, X2), .(X3, X4)) → U38_gga(X1, X2, X3, X4, gtcG_in_gg(X1, X3))
U36_gga(X1, X2, X3, X4, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, mergecC_in_gga(X2, .(X3, X4)))
U38_gga(X1, X2, X3, X4, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, mergecC_in_gga(.(X1, X2), X4))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U37_gga(X1, X2, X3, X4, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U39_gga(X1, X2, X3, X4, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
splitcD_in_ggaa(x0, x1)
mergesortcE_in_ga(x0)
U31_ggaa(x0, x1, x2)
U32_ga(x0, x1, x2, x3)
splitcA_in_gaa(x0)
U33_ga(x0, x1, x2, x3, x4)
U26_gaa(x0, x1, x2)
U34_ga(x0, x1, x2, x3, x4)
U35_ga(x0, x1, x2, x3)
mergecC_in_gga(x0, x1)
U36_gga(x0, x1, x2, x3, x4)
U38_gga(x0, x1, x2, x3, x4)
lecF_in_gg(x0, x1)
U37_gga(x0, x1, x2, x3, x4)
gtcG_in_gg(x0, x1)
U39_gga(x0, x1, x2, x3, x4)
U40_gg(x0, x1, x2)
U41_gg(x0, x1, x2)
MERGESORTE_IN_GA(.(X1, .(X2, X3))) → U4_GA(X1, X2, X3, U31_ggaa(X1, .(X2, X3), U26_gaa(X2, X3, splitcA_in_gaa(X3))))
POL(.(x1, x2)) = 2 + 2·x2
POL(0) = 0
POL(MERGESORTE_IN_GA(x1)) = 2·x1
POL(U26_gaa(x1, x2, x3)) = 2·x3
POL(U31_ggaa(x1, x2, x3)) = x3
POL(U32_ga(x1, x2, x3, x4)) = 1
POL(U33_ga(x1, x2, x3, x4, x5)) = 0
POL(U34_ga(x1, x2, x3, x4, x5)) = 0
POL(U35_ga(x1, x2, x3, x4)) = 0
POL(U36_gga(x1, x2, x3, x4, x5)) = 0
POL(U37_gga(x1, x2, x3, x4, x5)) = 0
POL(U38_gga(x1, x2, x3, x4, x5)) = 0
POL(U39_gga(x1, x2, x3, x4, x5)) = 0
POL(U40_gg(x1, x2, x3)) = 2·x3
POL(U41_gg(x1, x2, x3)) = 1 + x1
POL(U4_GA(x1, x2, x3, x4)) = 2·x4
POL(U6_GA(x1, x2, x3, x4, x5)) = 2·x4
POL([]) = 0
POL(gtcG_in_gg(x1, x2)) = 2 + 2·x1 + 2·x2
POL(gtcG_out_gg(x1, x2)) = x1
POL(lecF_in_gg(x1, x2)) = 0
POL(lecF_out_gg(x1, x2)) = 0
POL(mergecC_in_gga(x1, x2)) = 0
POL(mergecC_out_gga(x1, x2, x3)) = 0
POL(mergesortcE_in_ga(x1)) = 1
POL(mergesortcE_out_ga(x1, x2)) = 0
POL(s(x1)) = x1
POL(splitcA_in_gaa(x1)) = 2 + x1
POL(splitcA_out_gaa(x1, x2, x3)) = 2 + x2 + 2·x3
POL(splitcD_in_ggaa(x1, x2)) = 2 + x1 + x2
POL(splitcD_out_ggaa(x1, x2, x3, x4)) = x3 + x4
U4_GA(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → MERGESORTE_IN_GA(X5)
U4_GA(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U6_GA(X1, X2, X3, X6, mergesortcE_in_ga(X5))
U6_GA(X1, X2, X3, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6)
splitcD_in_ggaa(X1, X2) → U31_ggaa(X1, X2, splitcA_in_gaa(X2))
mergesortcE_in_ga([]) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3))) → U32_ga(X1, X2, X3, splitcD_in_ggaa(X1, .(X2, X3)))
U31_ggaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
U32_ga(X1, X2, X3, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X6, mergesortcE_in_ga(X5))
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, splitcA_in_gaa(X2))
U33_ga(X1, X2, X3, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X7, mergesortcE_in_ga(X6))
U26_gaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U34_ga(X1, X2, X3, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, mergecC_in_gga(X7, X8))
U35_ga(X1, X2, X3, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
mergecC_in_gga(X1, []) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga([], X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(.(X1, X2), .(X3, X4)) → U36_gga(X1, X2, X3, X4, lecF_in_gg(X1, X3))
mergecC_in_gga(.(X1, X2), .(X3, X4)) → U38_gga(X1, X2, X3, X4, gtcG_in_gg(X1, X3))
U36_gga(X1, X2, X3, X4, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, mergecC_in_gga(X2, .(X3, X4)))
U38_gga(X1, X2, X3, X4, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, mergecC_in_gga(.(X1, X2), X4))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U37_gga(X1, X2, X3, X4, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U39_gga(X1, X2, X3, X4, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
splitcD_in_ggaa(x0, x1)
mergesortcE_in_ga(x0)
U31_ggaa(x0, x1, x2)
U32_ga(x0, x1, x2, x3)
splitcA_in_gaa(x0)
U33_ga(x0, x1, x2, x3, x4)
U26_gaa(x0, x1, x2)
U34_ga(x0, x1, x2, x3, x4)
U35_ga(x0, x1, x2, x3)
mergecC_in_gga(x0, x1)
U36_gga(x0, x1, x2, x3, x4)
U38_gga(x0, x1, x2, x3, x4)
lecF_in_gg(x0, x1)
U37_gga(x0, x1, x2, x3, x4)
gtcG_in_gg(x0, x1)
U39_gga(x0, x1, x2, x3, x4)
U40_gg(x0, x1, x2)
U41_gg(x0, x1, x2)
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U19_GA(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U19_GA(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6), X7)
splitcD_in_ggaa(X1, X2, .(X1, X3), X4) → U31_ggaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U26_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U26_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U31_ggaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → U28_ga(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U28_ga(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U29_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U32_ga(X1, X2, X3, X4, splitcD_in_ggaa(X1, .(X2, X3), X5, X6))
U32_ga(X1, X2, X3, X4, splitcD_out_ggaa(X1, .(X2, X3), X5, X6)) → U33_ga(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U33_ga(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U34_ga(X1, X2, X3, X4, X7, mergesortcE_in_ga(X6, X8))
U34_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X6, X8)) → U35_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X1, X5)) → U36_gga(X1, X2, X3, X4, X5, lecF_in_gg(X1, X3))
lecF_in_gg(s(X1), s(X2)) → U40_gg(X1, X2, lecF_in_gg(X1, X2))
lecF_in_gg(0, s(X1)) → lecF_out_gg(0, s(X1))
lecF_in_gg(0, 0) → lecF_out_gg(0, 0)
U40_gg(X1, X2, lecF_out_gg(X1, X2)) → lecF_out_gg(s(X1), s(X2))
U36_gga(X1, X2, X3, X4, X5, lecF_out_gg(X1, X3)) → U37_gga(X1, X2, X3, X4, X5, mergecC_in_gga(X2, .(X3, X4), X5))
mergecC_in_gga(.(X1, X2), .(X3, X4), .(X3, X5)) → U38_gga(X1, X2, X3, X4, X5, gtcG_in_gg(X1, X3))
gtcG_in_gg(s(X1), s(X2)) → U41_gg(X1, X2, gtcG_in_gg(X1, X2))
gtcG_in_gg(s(X1), 0) → gtcG_out_gg(s(X1), 0)
U41_gg(X1, X2, gtcG_out_gg(X1, X2)) → gtcG_out_gg(s(X1), s(X2))
U38_gga(X1, X2, X3, X4, X5, gtcG_out_gg(X1, X3)) → U39_gga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X1, X2), X4, X5))
U39_gga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X1, X2), X4, X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X3, X5))
U37_gga(X1, X2, X3, X4, X5, mergecC_out_gga(X2, .(X3, X4), X5)) → mergecC_out_gga(.(X1, X2), .(X3, X4), .(X1, X5))
U35_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U29_ga(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U30_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U30_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U19_GA(X1, X2, X3, X4, splitcD_in_ggaa(X2, X3, X5, X6))
U19_GA(X1, X2, X3, X4, splitcD_out_ggaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6), X7)
splitcD_in_ggaa(X1, X2, .(X1, X3), X4) → U31_ggaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U31_ggaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U26_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U26_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
MERGESORTB_IN_GA(.(X1, .(X2, X3))) → U19_GA(X1, X2, X3, splitcD_in_ggaa(X2, X3))
U19_GA(X1, X2, X3, splitcD_out_ggaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6))
splitcD_in_ggaa(X1, X2) → U31_ggaa(X1, X2, splitcA_in_gaa(X2))
U31_ggaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, splitcA_in_gaa(X2))
U26_gaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
splitcD_in_ggaa(x0, x1)
U31_ggaa(x0, x1, x2)
splitcA_in_gaa(x0)
U26_gaa(x0, x1, x2)
MERGESORTB_IN_GA(.(X1, .(X2, X3))) → U19_GA(X1, X2, X3, U31_ggaa(X2, X3, splitcA_in_gaa(X3)))
U19_GA(X1, X2, X3, splitcD_out_ggaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6))
MERGESORTB_IN_GA(.(X1, .(X2, X3))) → U19_GA(X1, X2, X3, U31_ggaa(X2, X3, splitcA_in_gaa(X3)))
splitcD_in_ggaa(X1, X2) → U31_ggaa(X1, X2, splitcA_in_gaa(X2))
U31_ggaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, splitcA_in_gaa(X2))
U26_gaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
splitcD_in_ggaa(x0, x1)
U31_ggaa(x0, x1, x2)
splitcA_in_gaa(x0)
U26_gaa(x0, x1, x2)
U19_GA(X1, X2, X3, splitcD_out_ggaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6))
MERGESORTB_IN_GA(.(X1, .(X2, X3))) → U19_GA(X1, X2, X3, U31_ggaa(X2, X3, splitcA_in_gaa(X3)))
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, splitcA_in_gaa(X2))
U31_ggaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
U26_gaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
splitcD_in_ggaa(x0, x1)
U31_ggaa(x0, x1, x2)
splitcA_in_gaa(x0)
U26_gaa(x0, x1, x2)
splitcD_in_ggaa(x0, x1)
U19_GA(X1, X2, X3, splitcD_out_ggaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6))
MERGESORTB_IN_GA(.(X1, .(X2, X3))) → U19_GA(X1, X2, X3, U31_ggaa(X2, X3, splitcA_in_gaa(X3)))
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, splitcA_in_gaa(X2))
U31_ggaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
U26_gaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U31_ggaa(x0, x1, x2)
splitcA_in_gaa(x0)
U26_gaa(x0, x1, x2)
U31_ggaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_ggaa(X1, X2, .(X1, X3), X4)
POL(.(x1, x2)) = 1 + x2
POL(MERGESORTB_IN_GA(x1)) = 2 + 2·x1
POL(U19_GA(x1, x2, x3, x4)) = 2 + 2·x4
POL(U26_gaa(x1, x2, x3)) = 1 + x3
POL(U31_ggaa(x1, x2, x3)) = 2 + x3
POL([]) = 0
POL(splitcA_in_gaa(x1)) = x1
POL(splitcA_out_gaa(x1, x2, x3)) = x2 + x3
POL(splitcD_out_ggaa(x1, x2, x3, x4)) = 1 + x4
U19_GA(X1, X2, X3, splitcD_out_ggaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6))
MERGESORTB_IN_GA(.(X1, .(X2, X3))) → U19_GA(X1, X2, X3, U31_ggaa(X2, X3, splitcA_in_gaa(X3)))
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2)) → U26_gaa(X1, X2, splitcA_in_gaa(X2))
U26_gaa(X1, X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U31_ggaa(x0, x1, x2)
splitcA_in_gaa(x0)
U26_gaa(x0, x1, x2)